/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#11=ZERO30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓1. Introduction

␈↓ α∧␈↓␈↓ αT(McCarthy␈α⊗1959)␈α↔proposed␈α⊗a␈α⊗program␈α↔with␈α⊗"common␈α⊗sense"␈α↔that␈α⊗would␈α↔express␈α⊗its
␈↓ α∧␈↓knowledge␈α⊂about␈α⊂the␈α⊂world␈α⊂in␈α⊂general␈α⊂and␈α⊂about␈α⊂the␈α⊂particular␈α⊂problem␈α⊂in␈α⊂a␈α⊂suitable␈α⊂logical
␈↓ α∧␈↓language.␈α∞ It␈α∞would␈α∞then␈α∞reason␈α
in␈α∞this␈α∞language␈α∞attempting␈α∞to␈α
derive␈α∞a␈α∞sentence␈α∞of␈α∞the␈α∞form␈α
␈↓↓I
␈↓ α∧␈↓↓should␈α∂do␈α∂X␈↓␈α∂after␈α⊂which␈α∂it␈α∂would␈α∂do␈α∂␈↓↓X.␈↓␈α⊂This␈α∂approach␈α∂was␈α∂further␈α∂developed␈α⊂in␈α∂(McCarthy
␈↓ α∧␈↓1963)␈α
and␈α
(McCarthy␈α
and␈α
Hayes␈α
1969),␈α
but␈αby␈α
1969␈α
it␈α
was␈α
already␈α
clear␈α
that␈α
something␈αmore␈α
than
␈↓ α∧␈↓deduction␈α∂is␈α∂necessary␈α∞in␈α∂order␈α∂to␈α∞express␈α∂and␈α∂use␈α∞common␈α∂sense␈α∂knowledge.␈α∂ Further␈α∞analysis
␈↓ α∧␈↓showed␈αthat␈αwhat␈αwas␈αmissing␈αwas␈αthe␈αability␈αto␈αjump␈αto␈αthe␈αconclusion␈αthat␈αthe␈αfacts␈αtaken␈αinto
␈↓ α∧␈↓account␈α∪are␈α∀sufficient␈α∪to␈α∀solve␈α∪a␈α∪problem.␈α∀ The␈α∪best␈α∀way␈α∪of␈α∪expressing␈α∀this␈α∪ability␈α∀is␈α∪still
␈↓ α∧␈↓problematical, and this paper presents one candidate in several variants.

␈↓ α∧␈↓␈↓ αTEven␈αwhen␈αa␈αprogram␈αdoes␈αnot␈αreach␈αits␈αconclusions␈αby␈αmanipulating␈αsentences␈αin␈αa␈αformal
␈↓ α∧␈↓language,␈α
we␈αcan␈α
often␈αprofitably␈α
analyze␈αits␈α
behavior␈α
by␈αconsidering␈α
it␈αto␈α
␈↓↓believe␈↓␈αcertain␈α
sentences
␈↓ α∧␈↓when␈α∞it␈α∞is␈α∞in␈α∞certain␈α
states,␈α∞and␈α∞we␈α∞can␈α∞study␈α∞how␈α
these␈α∞␈↓↓ascribed␈α∞beliefs␈↓␈α∞change␈α∞with␈α∞time.␈α
 See
␈↓ α∧␈↓(McCarthy␈α
1979).␈α
 When␈α
we␈α
do␈α
this,␈α
we␈α
will␈α
again␈α
discover␈α
that␈α
successful␈α
programs␈α
must␈αjump␈α
to
␈↓ α∧␈↓conclusions.

␈↓ α∧␈↓␈↓ αT␈↓↓Circumscription␈αinduction␈↓␈αis␈αa␈αformalized␈α␈↓↓rule␈αof␈αconjecture␈↓␈αthat␈αcan␈αbe␈αused␈αalong␈αwith␈αthe
␈↓ α∧␈↓␈↓↓rules␈α
of␈αinference␈↓␈α
of␈α
first␈αorder␈α
logic.␈α
 A␈αcomputer␈α
program␈α
can␈αuse␈α
circumscription␈α
induction␈αto
␈↓ α∧␈↓conjecture␈α
that␈αthe␈α
known␈α
entities␈αof␈α
a␈α
given␈αkind␈α
are␈α
all␈αthere␈α
are.␈α
 We␈αwill␈α
show␈α
by␈αexamples
␈↓ α∧␈↓that␈αhumans␈αuse␈αsuch␈α"non-monotonic"␈αreasoning␈αand␈αthat␈αit␈αis␈αrequired␈αfor␈αintelligent␈αbehavior.
␈↓ α∧␈↓The␈αdefault␈αcase␈αreasoning␈αof␈αmany␈αcomputer␈αprograms␈αand␈αthe␈αuse␈αof␈αTHNOT␈αin␈αPLANNER
␈↓ α∧␈↓programs␈α∞are␈α∞also␈α∞examples␈α∞of␈α∞non-monotonic␈α∞reasoning,␈α∞but␈α∞possibly␈α∞of␈α∞a␈α∞different␈α∞kind␈α
from
␈↓ α∧␈↓those discussed in this paper.

␈↓ α∧␈↓␈↓ αTAll␈α∃the␈α∀well␈α∃known␈α∀languages␈α∃of␈α∀mathematical␈α∃logic␈α∀have␈α∃the␈α∃following␈α∀␈↓↓monotonicity
␈↓ α∧␈↓↓property␈↓.␈α If␈αa␈αsentence␈α␈↓↓p␈↓␈αfollows␈αfrom␈αa␈αcollection␈α␈↓↓A␈↓␈αof␈αsentences␈αand␈α␈↓↓A ⊂ B␈↓,␈αthen␈α␈↓↓p␈↓␈αfollows␈αfrom
␈↓ α∧␈↓␈↓↓B.␈↓␈α∂In␈α∂the␈α∂notation␈α∂of␈α∂proof␈α∂theory:␈α∂if␈α∂␈↓↓A ␈↓πr␈↓↓ p␈↓␈α∂and␈α∂␈↓↓A ⊂ B␈↓,␈α∂then␈α∂␈↓↓B ␈↓πr␈↓↓ p␈↓.␈α∂ Since␈α∂a␈α∂proof␈α⊂from␈α∂the
␈↓ α∧␈↓premisses␈α
␈↓↓A␈↓␈α
is␈α
a␈α
sequence␈α
of␈α
sentences␈α
each␈α
of␈αwhich␈α
is␈α
a␈α
either␈α
a␈α
premiss,␈α
an␈α
axiom␈α
or␈αfollows
␈↓ α∧␈↓from␈α
a␈α
subset␈α
of␈α
the␈α∞sentences␈α
occurring␈α
earlier␈α
in␈α
the␈α
proof␈α∞by␈α
one␈α
of␈α
the␈α
rules␈α
of␈α∞inference,␈α
a
␈↓ α∧␈↓proof␈α∩from␈α∩␈↓↓A␈↓␈α∪can␈α∩also␈α∩serve␈α∩as␈α∪a␈α∩proof␈α∩from␈α∩␈↓↓B␈↓␈α∪assuming␈α∩␈↓↓A ⊂ B␈↓.␈α∩ The␈α∩semantic␈α∪notion␈α∩of
␈↓ α∧␈↓entailment␈αis␈αalso␈αmonotonic;␈αwe␈αsay␈αthat␈α␈↓↓A␈↓␈αentails␈α␈↓↓p␈↓␈α(written␈α␈↓↓A ␈↓πq␈↓↓ p␈↓)␈αif␈α␈↓↓p␈↓␈αis␈αtrue␈αin␈αall␈αmodels␈αof
␈↓ α∧␈↓␈↓↓A.␈↓␈α
But␈α
if␈α␈↓↓A ␈↓πq␈↓↓ p␈↓␈α
and␈α
␈↓↓A ⊂ B␈↓,␈α
then␈αevery␈α
model␈α
of␈α
␈↓↓B␈↓␈αis␈α
also␈α
a␈α
model␈αof␈α
␈↓↓A,␈↓␈α
which␈α
shows␈αthat␈α
␈↓↓B ␈↓πq␈↓↓ p␈↓.
␈↓ α∧␈↓Some␈α
AI␈α∞reasoning␈α
systems␈α∞are␈α
non-monotonic,␈α∞because␈α
they␈α∞contain␈α
rules␈α∞of␈α
inference␈α∞that␈α
not
␈↓ α∧␈↓only␈α⊃require␈α⊃the␈α∩presence␈α⊃of␈α⊃premiss␈α∩sentences␈α⊃in␈α⊃the␈α⊃data␈α∩base␈α⊃matching␈α⊃their␈α∩patterns␈α⊃but
␈↓ α∧␈↓require the absence of sentences matching certain other patterns.

␈↓ α∧␈↓␈↓ αTThe␈α⊂result␈α∂of␈α⊂applying␈α∂circumscription␈α⊂induction␈α⊂to␈α∂a␈α⊂collection␈α∂␈↓↓A␈↓␈α⊂of␈α∂facts␈α⊂is␈α⊂a␈α∂sentence
␈↓ α∧␈↓schema␈α∞that␈α∂essentially␈α∞asserts␈α∞that␈α∂the␈α∞only␈α∞objects␈α∂satisfying␈α∞a␈α∞predicate␈α∂␈↓↓P(x)␈↓␈α∞are␈α∂those␈α∞whose
␈↓ α∧␈↓existence␈α
follows␈α
from␈α
the␈α
sentences␈α
of␈α
␈↓↓A.␈↓␈α
Since␈α
adding␈α
more␈α
sentences␈α
might␈α
require␈α
the␈α
existence
␈↓ α∧␈↓of␈αmore␈αobjects,␈αcircumscription␈αis␈αnot␈αmonotonic.␈α Conclusions␈αderived␈αfrom␈αcircumscription␈αmay
␈↓ α∧␈↓be␈αregarded␈αas␈αconsequences␈αof␈αconjecturing␈αthat␈α␈↓↓A␈↓␈αincludes␈αall␈αthe␈αrelevant␈αfacts.␈α An␈αintelligent
␈↓ α∧␈↓program␈α
might␈αmake␈α
such␈α
a␈αconjecture␈α
make␈α
a␈αplan␈α
on␈αthe␈α
basis␈α
of␈αthe␈α
conclusions␈α
reached.␈α It
␈↓ α∧␈↓might␈α⊂immediately␈α∂carry␈α⊂out␈α⊂the␈α∂plan,␈α⊂or␈α∂be␈α⊂more␈α⊂cautious␈α∂and␈α⊂look␈α∂for␈α⊂additional␈α⊂facts␈α∂that
␈↓ α∧␈↓might␈α
require␈α∞modifying␈α
it.␈α
 If␈α∞it␈α
comes␈α
to␈α∞reject␈α
the␈α
circumscription␈α∞conjecture,␈α
it␈α∞will␈α
normally
␈↓ α∧␈↓have␈α∞to␈α
circumscribe␈α∞again␈α
on␈α∞the␈α
basis␈α∞of␈α∞additional␈α
facts.␈α∞ It␈α
will␈α∞be␈α
necessary␈α∞to␈α∞␈↓↓assume␈↓␈α
that
␈↓ α∧␈↓everything␈α
relevant␈α
has␈αfinally␈α
been␈α
taken␈αinto␈α
account,␈α
except␈αin␈α
mathematical␈α
problems,␈αwhere␈α
it
␈↓ α∧␈↓can often be proved from the original statement of the problem.
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓␈↓ αTBefore␈α∩introducing␈α∩the␈α∩formalism,␈α∩we␈α∪present␈α∩an␈α∩example␈α∩showing␈α∩the␈α∩need␈α∪for␈α∩non-
␈↓ α∧␈↓monotonic reasoning.


␈↓ α∧␈↓αMissionaries and Cannibals

␈↓ α∧␈↓␈↓ αTThe␈α∞much␈α∂used␈α∞␈↓↓missionaries␈α∞and␈α∂cannibals␈↓␈α∞puzzle␈α∞contains␈α∂enough␈α∞detail␈α∞to␈α∂illustrate␈α∞the
␈↓ α∧␈↓issues.

␈↓ α∧␈↓␈↓ αT␈↓↓"Three␈α∪missionaries␈α∀and␈α∪three␈α∀cannibals␈α∪come␈α∀to␈α∪a␈α∪river.␈α∀ A␈α∪rowboat␈α∀that␈α∪seats␈α∀two␈α∪is
␈↓ α∧␈↓↓available.␈α∪ If␈α∩the␈α∪cannibals␈α∩ever␈α∪outnumber␈α∪the␈α∩missionaries␈α∪on␈α∩either␈α∪bank␈α∩of␈α∪the␈α∪river,␈α∩the
␈↓ α∧␈↓↓missionaries will be eaten.  How shall they cross the river?"␈↓.

␈↓ α∧␈↓␈↓ αTObviously␈α
the␈α∞puzzler␈α
is␈α
expected␈α∞to␈α
devise␈α
a␈α∞strategy␈α
of␈α
rowing␈α∞the␈α
boat␈α
back␈α∞and␈α
forth
␈↓ α∧␈↓that gets them all across and avoids the disaster.

␈↓ α∧␈↓␈↓ αTAmarel␈α∩(1971)␈α∩considered␈α∩several␈α∩representations␈α⊃of␈α∩the␈α∩problem␈α∩and␈α∩discussed␈α⊃criteria
␈↓ α∧␈↓whereby␈α⊂the␈α⊃following␈α⊂representation␈α⊂is␈α⊃preferred␈α⊂for␈α⊂purposes␈α⊃of␈α⊂AI,␈α⊂because␈α⊃it␈α⊂leads␈α⊃to␈α⊂the
␈↓ α∧␈↓smallest␈αstate␈αspace␈αthat␈αmust␈αbe␈αexplored␈αto␈αfind␈αthe␈αsolution.␈α A␈αstate␈αis␈αa␈αtriple␈αcomprising␈αthe
␈↓ α∧␈↓numbers␈αof␈αmissionaries,␈αcannibals␈αand␈αboats␈αon␈αthe␈αstarting␈αbank␈αof␈αthe␈αriver.␈α The␈αinitial␈αstate
␈↓ α∧␈↓is␈α≤331,␈α≤the␈α≤desired␈α≤final␈α≤state␈α≤is␈α≤000,␈α≤and␈α≤one␈α≤solution␈α≤is␈α≤given␈α≤by␈α≤the␈α≠sequence
␈↓ α∧␈↓(331,220,321,300,311,110,221,020,031,010,021,000).

␈↓ α∧␈↓␈↓ αTWe␈α⊂are␈α⊂not␈α⊂presently␈α⊂concerned␈α⊂with␈α⊂the␈α⊂heuristics␈α⊂of␈α⊂the␈α⊂problem␈α⊂but␈α⊂rather␈α⊂with␈α⊂the
␈↓ α∧␈↓correctness␈αof␈αthe␈αreasoning␈αthat␈α
goes␈αfrom␈αthe␈αEnglish␈αstatement␈α
of␈αthe␈αproblem␈αto␈αAmarel's␈α
state
␈↓ α∧␈↓space␈α
representation.␈α
 A␈α∞generally␈α
intelligent␈α
computer␈α∞program␈α
should␈α
be␈α∞able␈α
to␈α
carry␈α∞out␈α
this
␈↓ α∧␈↓reasoning.␈α⊃ Of␈α⊃course,␈α⊃there␈α⊃are␈α⊃the␈α⊃well␈α⊃known␈α⊃difficulties␈α⊃in␈α⊃making␈α⊃computers␈α⊂understand
␈↓ α∧␈↓English,␈α⊃but␈α⊃suppose␈α⊃the␈α⊃English␈α⊃sentences␈α⊃describing␈α⊃the␈α⊃problem␈α⊃have␈α⊃already␈α⊃been␈α⊃rather
␈↓ α∧␈↓directly␈α⊂translated␈α⊂into␈α⊂first␈α⊂order␈α⊂logic.␈α⊂ The␈α⊂correctness␈α⊂of␈α⊂Amarel's␈α⊂representation␈α⊂is␈α⊃not␈α⊂an
␈↓ α∧␈↓ordinary logical consequence of these sentences for two further reasons.

␈↓ α∧␈↓␈↓ αTFirst,␈α∞nothing␈α∞has␈α∞been␈α∞stated␈α∞about␈α∞the␈α∞properties␈α∞of␈α∞boats␈α∞or␈α∞even␈α∞the␈α∞fact␈α∞that␈α
rowing
␈↓ α∧␈↓across␈α∞the␈α∞river␈α
doesn't␈α∞change␈α∞the␈α∞numbers␈α
of␈α∞missionaries␈α∞or␈α∞cannibals␈α
or␈α∞the␈α∞capacity␈α∞of␈α
the
␈↓ α∧␈↓boat.␈α Indeed␈αit␈αhasn't␈αbeen␈αstated␈αthat␈αsituations␈αchange␈αas␈αa␈αresult␈αof␈αaction.␈α These␈αfacts␈αfollow
␈↓ α∧␈↓from␈α∞common␈α∞sense␈α∞knowledge,␈α∞so␈α∞let␈α∞us␈α
imagine␈α∞that␈α∞common␈α∞sense␈α∞knowledge,␈α∞or␈α∞at␈α∞least␈α
the
␈↓ α∧␈↓relevant part of it, is also expressed in first order logic.

␈↓ α∧␈↓␈↓ αTThe␈α∩second␈α⊃reason␈α∩we␈α⊃can't␈α∩␈↓↓deduce␈↓␈α∩the␈α⊃propriety␈α∩of␈α⊃Amarel's␈α∩representation␈α∩is␈α⊃deeper.
␈↓ α∧␈↓Imagine␈α
giving␈α
someone␈α
the␈α
problem,␈α
and␈α
after␈αhe␈α
puzzles␈α
for␈α
a␈α
while,␈α
he␈α
suggests␈αgoing␈α
upstream
␈↓ α∧␈↓half␈α
a␈α
mile␈α
and␈α
crossing␈α
on␈α
a␈α
bridge.␈α∞ "What␈α
bridge",␈α
you␈α
say.␈α
 "No␈α
bridge␈α
is␈α
mentioned␈α∞in␈α
the
␈↓ α∧␈↓statement␈αof␈α
the␈αproblem."␈αAnd␈α
this␈αdunce␈αreplies,␈α
"Well,␈αthey␈α
don't␈αsay␈αthere␈α
isn't␈αa␈αbridge".␈α
 You
␈↓ α∧␈↓look␈αat␈αthe␈αEnglish␈αand␈αeven␈αat␈αthe␈αtranslation␈αof␈αthe␈αEnglish␈αinto␈αfirst␈αorder␈αlogic,␈αand␈αyou␈αmust
␈↓ α∧␈↓admit␈αthat␈α
"they␈αdon't␈αsay"␈α
there␈αis␈αno␈α
bridge.␈α So␈αyou␈α
modify␈αthe␈αproblem␈α
to␈αexclude␈αbridges␈α
and
␈↓ α∧␈↓pose␈α∂it␈α∂again,␈α∂and␈α∂the␈α∂dunce␈α∂proposes␈α∂a␈α∂helicopter,␈α∂and␈α∂after␈α∂you␈α∂exclude␈α∂that,␈α∂he␈α∂proposes␈α∂a
␈↓ α∧␈↓winged horse or that the others hang onto the outside of the boat while two row.

␈↓ α∧␈↓␈↓ αTYou␈α
now␈α∞see␈α
that␈α
while␈α∞a␈α
dunce,␈α∞he␈α
is␈α
an␈α∞inventive␈α
dunce.␈α
 Despairing␈α∞of␈α
getting␈α∞him␈α
to
␈↓ α∧␈↓accept␈α⊂the␈α⊂problem␈α⊂in␈α⊂the␈α⊂proper␈α⊂puzzler's␈α⊂spirit,␈α⊂you␈α⊂tell␈α⊂him␈α⊂the␈α⊂solution.␈α⊂ To␈α⊃your␈α⊂further
␈↓ α∧␈↓annoyance,␈αhe␈αattacks␈αyour␈αsolution␈αon␈αthe␈αgrounds␈αthat␈αthe␈αboat␈αmight␈αhave␈αa␈αleak␈αor␈αlack␈αoars.
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓After␈αyou␈αrectify␈αthat␈αomission␈αfrom␈αthe␈αstatement␈αof␈αthe␈αproblem,␈αhe␈αsuggests␈αthat␈αa␈αsea␈αmonster
␈↓ α∧␈↓may␈αswim␈αup␈αthe␈αriver␈αand␈αmay␈αswallow␈αthe␈αboat.␈α Again␈αyou␈αare␈αfrustrated,␈αand␈αyou␈αlook␈αfor␈αa
␈↓ α∧␈↓mode of reasoning that will settle his hash once and for all.

␈↓ α∧␈↓␈↓ αTIn␈αspite␈α
of␈αour␈α
irritation␈αwith␈αthe␈α
dunce,␈αit␈α
would␈αbe␈αcheating␈α
to␈αput␈α
into␈αthe␈α
statement␈αof
␈↓ α∧␈↓the␈α
problem␈α
that␈α
there␈α
is␈α
no␈αother␈α
way␈α
to␈α
cross␈α
the␈α
river␈αthan␈α
using␈α
the␈α
boat␈α
and␈α
that␈αnothing␈α
can
␈↓ α∧␈↓go␈αwrong␈α
with␈αthe␈α
boat.␈α A␈αhuman␈α
doesn't␈αneed␈α
such␈αan␈αad␈α
hoc␈αnarrowing␈α
of␈αthe␈α
problem,␈αand
␈↓ α∧␈↓indeed␈αthe␈αonly␈αwatertight␈αway␈αto␈αdo␈αit␈αmight␈αamount␈αto␈αspecifying␈αthe␈αAmarel␈αrepresentation␈αin
␈↓ α∧␈↓English.␈α Rather␈α
we␈αwant␈αto␈α
avoid␈αthe␈α
excessive␈αqualification␈αand␈α
get␈αthe␈α
Amarel␈αrepresentation
␈↓ α∧␈↓by common sense reasoning as humans ordinarily do.

␈↓ α∧␈↓␈↓ αTCircumscription␈αis␈αone␈αcandidate␈αfor␈αaccomplishing␈αthis.␈α It␈αwill␈αallow␈αus␈αto␈αconjecture␈αthat
␈↓ α∧␈↓no␈αrelevant␈α
entities␈αexist␈αexcept␈α
those␈αwhose␈αexistence␈α
follows␈αfrom␈αthe␈α
statement␈αof␈α
the␈αproblem
␈↓ α∧␈↓and␈α∩common␈α∪sense␈α∩knowledge.␈α∩ When␈α∪we␈α∩␈↓↓circumscribe␈↓␈α∪the␈α∩first␈α∩order␈α∪logic␈α∩statement␈α∪of␈α∩the
␈↓ α∧␈↓problem␈α
together␈α
with␈α
the␈α
common␈α
sense␈α
facts␈α
about␈α
boats␈α
etc.,␈α
we␈α
will␈α
be␈α
able␈α
to␈α
conclude␈α
that
␈↓ α∧␈↓there␈αis␈αno␈αbridge␈αor␈αhelicopter.␈α "Aha",␈αyou␈αsay,␈α"but␈αthere␈αwon't␈αbe␈αany␈αoars␈αeither".␈α No,␈αwe␈αget
␈↓ α∧␈↓out␈αof␈αthat␈αas␈αfollows:␈αIt␈αis␈αa␈αpart␈αof␈αcommon␈αknowledge␈αthat␈αa␈αboat␈αcan␈αbe␈αused␈αto␈αcross␈αa␈αriver
␈↓ α∧␈↓␈↓↓unless␈αthere␈αis␈αsomething␈α
wrong␈αwith␈αit␈αor␈α
something␈αelse␈αprevents␈αusing␈α
it␈↓,␈αand␈αif␈αour␈α
facts␈αdon't
␈↓ α∧␈↓require␈αthat␈αthere␈αbe␈αsomething␈αthat␈αprevents␈αcrossing␈αthe␈αriver,␈αcircumscription␈αwill␈αgenerate␈αthe
␈↓ α∧␈↓conjecture␈αthat␈α
there␈αisn't.␈α
 The␈αprice␈α
is␈αintroducing␈αas␈α
entities␈αin␈α
our␈αlanguage␈α
the␈α"somethings"
␈↓ α∧␈↓that may prevent the use of the boat.

␈↓ α∧␈↓␈↓ αTIf␈α
the␈αstatement␈α
of␈α
the␈αproblem␈α
were␈α
extended␈αto␈α
mention␈α
a␈αbridge,␈α
then␈αthe␈α
circumscription
␈↓ α∧␈↓of␈α∞the␈α∞problem␈α∞statement␈α∞would␈α∞no␈α∞longer␈α∂permit␈α∞showing␈α∞the␈α∞non-existence␈α∞of␈α∞a␈α∞bridge,␈α∂i.e.␈α∞a
␈↓ α∧␈↓conclusion␈α
that␈α
can␈α
be␈α∞drawn␈α
from␈α
a␈α
smaller␈α∞collection␈α
of␈α
facts␈α
can␈α∞no␈α
longer␈α
be␈α
drawn␈α∞from␈α
a
␈↓ α∧␈↓larger.␈α∞ This␈α∞non-monotonic␈α∞character␈α∞of␈α∞circumscription␈α∞is␈α
just␈α∞what␈α∞we␈α∞want␈α∞for␈α∞this␈α∞kind␈α
of
␈↓ α∧␈↓problem.␈α∞ The␈α∞statement,␈α∞␈↓↓"There␈α∞is␈α∞a␈α∞bridge␈α∞a␈α
mile␈α∞upstream,␈α∞and␈α∞the␈α∞boat␈α∞has␈α∞a␈α∞leak."␈↓␈α
doesn't
␈↓ α∧␈↓contradict the text of the problem, but its addition invalidates the Amarel representation.

␈↓ α∧␈↓␈↓ αTIn␈αthe␈αusual␈αsort␈αof␈αpuzzle,␈αthere␈αis␈αa␈αconvention␈αthat␈αthere␈αis␈αno␈αadditional␈αobjects␈αbeyond
␈↓ α∧␈↓those␈αmentioned␈αin␈αthe␈αpuzzle␈αor␈αwhose␈αexistence␈αis␈αdeducible␈αfrom␈αthe␈αpuzzle␈αand␈αcommon␈αsense
␈↓ α∧␈↓knowledge.␈α The␈αconvention␈αcan␈αbe␈αexplicated␈α
as␈αapplying␈αcircumscription␈αto␈αthe␈αpuzzle␈α
statement
␈↓ α∧␈↓and␈α∞a␈α∞certain␈α∞part␈α∞of␈α∞common␈α∞sense␈α∞knowledge.␈α∞ However,␈α∞if␈α∞one␈α∞really␈α∞were␈α∞sitting␈α∞by␈α∞a␈α
river
␈↓ α∧␈↓bank␈α→and␈α_these␈α→six␈α_people␈α→came␈α→by␈α_and␈α→posed␈α_their␈α→problem,␈α_one␈α→wouldn't␈α→take␈α_the
␈↓ α∧␈↓circumscription␈α
for␈αgranted,␈α
but␈αone␈α
would␈αconsider␈α
the␈αresult␈α
of␈αcircumscripion␈α
as␈α
a␈αhypothesis.
␈↓ α∧␈↓Thus circumscription must be used as a mode of conjecture.

␈↓ α∧␈↓␈↓ αTAt␈α⊂first␈α⊂I␈α⊂considered␈α⊂this␈α⊂solution␈α⊂ad␈α⊂hoc,␈α⊂but␈α⊂I␈α⊂am␈α⊂now␈α⊂convinced␈α⊂that␈α⊂it␈α⊂is␈α⊃a␈α⊂correct
␈↓ α∧␈↓explication␈αof␈αthe␈αuse␈αof␈α␈↓↓normality␈↓;␈αi.e.␈αunless␈αsomething␈αabnormal␈αexists,␈αan␈αobject␈αcan␈αbe␈αused␈α
to
␈↓ α∧␈↓carry out its normal function.

␈↓ α∧␈↓␈↓ αTSome␈α∂have␈α∂suggested␈α∂that␈α∂the␈α∂difficulties␈α∂might␈α∂be␈α∂avoided␈α∂by␈α∂introducing␈α∂probabilities.
␈↓ α∧␈↓They␈α∞suggest␈α∞that␈α∞the␈α
existence␈α∞of␈α∞a␈α∞bridge␈α∞is␈α
improbable.␈α∞ Well,␈α∞the␈α∞whole␈α∞situation␈α
involving
␈↓ α∧␈↓cannibals␈α∂with␈α⊂the␈α∂postulated␈α⊂properties␈α∂is␈α⊂so␈α∂improbable␈α⊂that␈α∂it␈α⊂is␈α∂hard␈α⊂to␈α∂take␈α⊂seriously␈α∂the
␈↓ α∧␈↓conditional␈α⊃probability␈α⊃of␈α∩a␈α⊃bridge␈α⊃given␈α⊃the␈α∩hypotheses.␈α⊃ Moreover,␈α⊃we␈α⊃mentally␈α∩propose␈α⊃to
␈↓ α∧␈↓ourselves␈α~the␈α~normal␈α≠non-bridge␈α~non-sea-monster␈α~interpretation␈α~␈↓↓before␈↓␈α≠considering␈α~these
␈↓ α∧␈↓extraneous␈α
possibilities,␈α
let␈α
alone␈α
their␈α
probabilities,␈α
i.e.␈α
we␈α
usually␈α
don't␈α
even␈α
introduce␈α
the␈α
sample
␈↓ α∧␈↓space␈αin␈αwhich␈αthese␈αpossibilities␈αare␈αassigned␈αwhatever␈αprobabilities␈αone␈αmight␈αconsider␈αthem␈αto
␈↓ α∧␈↓have.␈α Therefore,␈αregardless␈αof␈αour␈αknowledge␈αof␈αprobabilities,␈αwe␈αneed␈αa␈αway␈αof␈αformulating␈αthe
␈↓ α∧␈↓␈↓ u4


␈↓ α∧␈↓normal␈α∩situation␈α∩from␈α∩the␈α⊃statement␈α∩of␈α∩the␈α∩facts,␈α⊃and␈α∩non-monotonic␈α∩reasoning␈α∩seems␈α∩to␈α⊃be
␈↓ α∧␈↓required.

␈↓ α∧␈↓␈↓ αTUsing␈α
circumscription␈α
requires␈α
that␈α
common␈α
sense␈α
knowledge␈α
be␈α
expressed␈α
in␈α
a␈α∞form␈α
that
␈↓ α∧␈↓says␈α
a␈αboat␈α
can␈αbe␈α
used␈αto␈α
cross␈αrivers␈α
unless␈αthere␈α
is␈αsomething␈α
wrong␈αwith␈α
it.␈α In␈α
particular,␈αit
␈↓ α∧␈↓looks␈α⊂like␈α⊂we␈α∂must␈α⊂introduce␈α⊂into␈α⊂our␈α∂␈↓↓ontology␈↓␈α⊂(the␈α⊂things␈α⊂that␈α∂exist)␈α⊂a␈α⊂category␈α⊂that␈α∂includes
␈↓ α∧␈↓␈↓↓something␈α⊃wrong␈α⊃with␈α⊃a␈α⊃boat␈↓␈α⊃or␈α⊃a␈α⊃category␈α⊃that␈α⊃includes␈α⊃␈↓↓something␈α⊃that␈α⊃may␈α⊃prevent␈α∩its␈α⊃use␈↓.
␈↓ α∧␈↓Incidentally,␈α∂once␈α∂we␈α∂have␈α∂decided␈α∂to␈α∂admit␈α∞␈↓↓something␈α∂wrong␈α∂with␈α∂the␈α∂boat␈↓,␈α∂we␈α∂are␈α∂inclined␈α∞to
␈↓ α∧␈↓admit␈α
a␈α
␈↓↓lack␈α
of␈αoars␈↓␈α
as␈α
such␈α
a␈αsomething␈α
and␈α
to␈α
ask␈αquestions␈α
like,␈α
␈↓↓"Is␈α
a␈αlack␈α
of␈α
oars␈α
all␈α
that␈αis
␈↓ α∧␈↓↓wrong with the boat?␈↓".

␈↓ α∧␈↓␈↓ αTI␈α∩imagine␈α∩that␈α∪many␈α∩philosophers␈α∩and␈α∩scientists␈α∪would␈α∩be␈α∩reluctant␈α∩to␈α∪introduce␈α∩such
␈↓ α∧␈↓␈↓↓things,␈↓␈α
but␈α
the␈αfact␈α
that␈α
ordinary␈α
language␈αallows␈α
␈↓↓"something␈α
wrong␈αwith␈α
the␈α
boat"␈↓␈α
suggests␈αthat
␈↓ α∧␈↓we␈α
shouldn't␈α
be␈α
hasty␈α
in␈α
excluding␈α
it.␈α
 Making␈α
a␈α
suitable␈α
formalism␈α
may␈α
be␈α
technically␈αdifficult
␈↓ α∧␈↓and philosophically problematical, but we must try.

␈↓ α∧␈↓␈↓ αTWe␈α⊃challenge␈α⊂anyone␈α⊃who␈α⊃thinks␈α⊂he␈α⊃can␈α⊃avoid␈α⊂such␈α⊃entities␈α⊃to␈α⊂express␈α⊃in␈α⊃his␈α⊂favorite
␈↓ α∧␈↓formalism,␈α
␈↓↓"Besides␈αleakiness,␈α
there␈α
is␈αsomething␈α
else␈α
wrong␈αwith␈α
the␈α
boat"␈↓.␈α A␈α
good␈αsolution␈α
would
␈↓ α∧␈↓avoid counterfactuals as this one does.

␈↓ α∧␈↓␈↓ αTWe␈α∩hope␈α⊃circumscription␈α∩will␈α⊃help␈α∩understand␈α⊃natural␈α∩language,␈α⊃because␈α∩if␈α⊃the␈α∩use␈α⊃of
␈↓ α∧␈↓natural␈αlanguage␈αinvolves␈αsomething␈αlike␈αcircumscription,␈αit␈αis␈αunderstandable␈αthat␈αthe␈αexpression
␈↓ α∧␈↓of general common sense facts into natural language will seem implausible.


␈↓ α∧␈↓αCo-ordinate systems and propositional calculus circumscription.

␈↓ α∧␈↓␈↓ αTSuppose␈α⊃we␈α⊃want␈α⊃to␈α⊂establish␈α⊃a␈α⊃language␈α⊃in␈α⊃which␈α⊂to␈α⊃express␈α⊃some␈α⊃class␈α⊃of␈α⊂assertions.
␈↓ α∧␈↓Deciding␈α∪on␈α∀predicate␈α∪and␈α∪function␈α∀symbols␈α∪and␈α∀their␈α∪meanings␈α∪in␈α∀order␈α∪to␈α∀express␈α∪these
␈↓ α∧␈↓assertions␈α
is␈α
like␈αchoosing␈α
a␈α
co-ordinate␈αsystem␈α
for␈α
a␈αphysical␈α
space.␈α
 For␈αexample,␈α
in␈α
the␈αblocks
␈↓ α∧␈↓world␈α
one␈αmay␈α
express␈α
everything␈αin␈α
terms␈α
of␈αthe␈α
relation␈α␈↓↓on(x,y,s)␈↓␈α
meaning␈α
that␈αblock␈α
␈↓↓x␈↓␈α
is␈αon
␈↓ α∧␈↓block␈α␈↓↓y␈↓␈αin␈αsituation␈α␈↓↓s,␈↓␈αbut␈αone␈αmight␈αalso␈αuse␈αthe␈αrelation␈α␈↓↓above(x,y,s)␈↓␈αthat␈αwould␈αbe␈αsatisfied␈αif
␈↓ α∧␈↓there␈αwere␈αintervening␈αblocks␈αin␈αbetween␈α␈↓↓x␈↓␈αand␈α␈↓↓y.␈↓␈αThe␈αsame␈αassertions␈αabout␈αblocks␈αcan␈αbe␈α
made
␈↓ α∧␈↓in␈α
in␈α
either␈α
language.␈α
 In␈α
particular,␈α
each␈α
can␈αbe␈α
defined␈α
in␈α
terms␈α
of␈α
the␈α
other,␈α
and␈αequivalent␈α
sets
␈↓ α∧␈↓of␈αaxioms␈αcan␈αbe␈αwritten.␈α (I␈αdon't␈αknow␈αof␈αany␈αgeneral␈αstudy␈αof␈α"logical␈αco-ordinate␈αsystems"␈αand
␈↓ α∧␈↓their␈α
relations␈α∞and␈α
transformations.␈α∞ It␈α
will␈α∞certainly␈α
be␈α
more␈α∞complex␈α
than␈α∞the␈α
theory␈α∞of␈α
linear
␈↓ α∧␈↓transformations of vector spaces).

␈↓ α∧␈↓␈↓ αTLogical␈αco-ordinate␈α
systems␈αthat␈α
are␈αequivalent␈α
in␈αterms␈αof␈α
what␈αcan␈α
be␈αexpressed␈α
may␈αbe
␈↓ α∧␈↓inequivalent␈α⊃heuristically.␈α⊂ Conjectures␈α⊃that␈α⊂are␈α⊃natural␈α⊂in␈α⊃one␈α⊂system␈α⊃may␈α⊂seem␈α⊃contrived␈α⊂in
␈↓ α∧␈↓others.␈α In␈αparticular,␈αcircumscription␈αyields␈αdifferent␈αconjectures␈αin␈αdifferent␈αco-ordinate␈αsystems.
␈↓ α∧␈↓A propositional calculus version of circumscription illustrates some of the issues.

␈↓ α∧␈↓␈↓ αTA␈αpropositional␈αlanguage␈αfor␈αexpressing␈α
some␈αclass␈αof␈αassertions␈αis␈αestablished␈α
by␈αchoosing
␈↓ α∧␈↓propositional␈α∞letters␈α∞␈↓↓p␈↓β1␈↓↓,...,p␈↓βn␈↓␈α∞and␈α∞regarding␈α∞each␈α
of␈α∞them␈α∞as␈α∞expressing␈α∞some␈α∞elementary␈α
fact.
␈↓ α∧␈↓We␈αmay␈αthen␈αexpress␈αthe␈αset␈α␈↓↓A␈↓␈αof␈αknown␈αfacts␈αas␈αa␈αsentence␈α␈↓↓AX␈↓␈αin␈αterms␈αof␈αthe␈α␈↓↓p␈↓'s.␈α A␈αmodel␈αof
␈↓ α∧␈↓the facts is any assignment of truth values to the ␈↓↓p␈↓βi␈↓'s that makes ␈↓↓AX␈↓ true.

␈↓ α∧␈↓␈↓ αTAs␈α
a␈αsimple␈α
example,␈αwe␈α
may␈αbe␈α
thinking␈αof␈α
assertions␈α␈↓↓p,␈↓␈α
␈↓↓q,␈↓␈αand␈α
␈↓↓r␈↓␈αrelated␈α
by␈α␈↓↓p ≡ (q ≡ r)␈↓.
␈↓ α∧␈↓␈↓ u5


␈↓ α∧␈↓and␈α
satisfying␈α␈↓↓p ∨ r␈↓.␈α
 One␈α
co-ordinate␈αsystem␈α
would␈αtake␈α
␈↓↓p␈↓β1␈↓↓ = p␈↓␈α
and␈α␈↓↓p␈↓β2␈↓↓ = q␈↓,␈α
and␈α
another␈αwould
␈↓ α∧␈↓take ␈↓↓p␈↓β1␈↓↓' = q␈↓ and ␈↓↓p␈↓β2␈↓↓' = ¬(p ≡ r)␈↓.  In one system we would have the axiom ␈↓↓p␈↓β1␈↓↓

␈↓ α∧␈↓***********

␈↓ α∧␈↓␈↓ αTLet ␈↓↓M1␈↓ and ␈↓↓M2␈↓ be models of ␈↓↓AX.␈↓ We define

␈↓ α∧␈↓␈↓ αT␈↓↓M1 ≤ M2 ≡ ∀i.(true(p␈↓βi␈↓↓,M2) ⊃ true(p␈↓βi␈↓↓,M1))␈↓.

␈↓ α∧␈↓A␈α
minimal␈α
model␈α
is␈α
one␈α
that␈α
is␈α
not␈αa␈α
proper␈α
extension,␈α
i.e.␈α
a␈α
model␈α
in␈α
which␈α
(roughly␈αspeaking)␈α
as
␈↓ α∧␈↓many␈αof␈α
the␈α␈↓↓p␈↓βi␈↓s␈αas␈α
possible␈αare␈αfalse␈α
-␈αconsistent␈α
with␈αthe␈αtruth␈α
of␈α␈↓↓AX␈↓.␈α ␈↓↓Note␈α
that␈αwhile␈αthe␈α
models
␈↓ α∧␈↓↓of␈αa␈αset␈αof␈αfacts␈αare␈αindependent␈αof␈αthe␈αco-ordinate␈αsystem,␈αthe␈αminimal␈αmodels␈αdepend␈αon␈αthe␈αco-
␈↓ α∧␈↓↓ordinate␈αsystem␈↓.␈α Here␈αis␈αthe␈αmost␈αtrivial␈αexample.␈α Let␈αthere␈αbe␈αone␈αletter␈α␈↓↓p␈↓␈αrepresenting␈αthe␈αone
␈↓ α∧␈↓fact␈α∞in␈α
a␈α∞co-ordinate␈α
system␈α∞␈↓↓C,␈↓␈α
and␈α∞let␈α
␈↓↓A␈↓␈α∞be␈α
the␈α∞null␈α
set␈α∞of␈α
facts␈α∞so␈α
that␈α∞␈↓↓AX␈↓␈α
is␈α∞the␈α∞sentence␈α
␈↓↓T␈↓
␈↓ α∧␈↓(identically␈α∂true).␈α⊂ The␈α∂one␈α∂other␈α⊂co-ordinate␈α∂system␈α⊂␈↓↓C'␈↓␈α∂uses␈α∂the␈α⊂elementary␈α∂sentence␈α⊂␈↓↓p'␈↓␈α∂taken
␈↓ α∧␈↓equivalent␈α
to␈α
␈↓↓¬p␈↓.␈α
 The␈α
minimal␈α
model␈α
of␈α
␈↓↓C␈↓␈α
is␈α{¬p},␈α
and␈α
the␈α
minimal␈α
model␈α
of␈α
␈↓↓C'␈↓␈α
is␈α
{p}.␈α Since
␈↓ α∧␈↓minimal␈α∞reasoning␈α
depends␈α∞on␈α
the␈α∞co-ordinate␈α
system␈α∞and␈α
not␈α∞merely␈α
on␈α∞the␈α
facts␈α∞expressed␈α
in
␈↓ α∧␈↓the␈αaxioms,␈αthe␈αutility␈αof␈αan␈αaxiom␈αsystem␈αwill␈αdepend␈αon␈αwhether␈αits␈αminimal␈αmodels␈αexpress␈α
the
␈↓ α∧␈↓uses we wish to make of Occam's razor.

␈↓ α∧␈↓␈↓ αTA␈α∪less␈α∩trivial␈α∪example␈α∩of␈α∪minimal␈α∩entailment␈α∪is␈α∩the␈α∪following.␈α∩ The␈α∪propositional␈α∩co-
␈↓ α∧␈↓ordinate␈α
system␈α∞has␈α
basic␈α
sentences␈α∞␈↓↓p␈↓β1␈↓,␈α
␈↓↓p␈↓β2␈↓␈α
and␈α∞␈↓↓p␈↓β3␈↓,␈α
and␈α
␈↓↓AX␈α∞=␈α
p␈↓β1␈↓↓␈α
∨␈α∞p␈↓β2␈↓.␈α
 There␈α
are␈α∞two␈α
minimal
␈↓ α∧␈↓models.␈α
 ␈↓↓p␈↓β3␈↓␈α
is␈α
false␈αin␈α
both,␈α
and␈α
␈↓↓p␈↓β1␈↓␈αis␈α
false␈α
in␈α
one,␈αand␈α
␈↓↓p␈↓β2␈↓␈α
is␈α
false␈αin␈α
the␈α
other.␈α
 Thus␈α
we␈αhave
␈↓ α∧␈↓␈↓↓AX ␈↓πq␈↓βm␈↓↓ (¬(p␈↓β1␈↓↓ ∧ p␈↓β2␈↓↓) ∧ ¬p␈↓β3␈↓).

␈↓ α∧␈↓␈↓ αTNote␈α
that␈αif␈α
␈↓↓AX␈↓␈αis␈α
a␈α
conjunction␈αof␈α
certain␈αelementary␈α
sentences␈α
(some␈αof␈α
them␈αnegated),␈α
e.g.
␈↓ α∧␈↓␈↓↓AX = p␈↓β2␈↓↓ ∧ ¬p␈↓β4␈↓,␈α∂then␈α⊂there␈α∂is␈α⊂a␈α∂unique␈α⊂minimal␈α∂model,␈α⊂but␈α∂if,␈α⊂as␈α∂above,␈α⊂␈↓↓AX = p␈↓β2␈↓↓ ∨ ¬p␈↓β4␈↓,␈α∂then
␈↓ α∧␈↓there is more than one minimal model.

␈↓ α∧␈↓␈↓ αTOne may also consider extensions ␈↓↓relative␈↓ to a set ␈↓↓B␈↓ of elementary sentences.  We have

␈↓ α∧␈↓␈↓ αT␈↓↓M1 ≤ M2 (mod B) ≡ ∀p.(p ε B ∧ true(p,M1) ⊃ true(p,M2)␈↓.

␈↓ α∧␈↓We␈α⊂can␈α⊂then␈α⊂introduce␈α⊂minimal␈α⊂models␈α⊂relative␈α⊂to␈α⊂␈↓↓B␈↓␈α⊂and␈α⊂the␈α⊂corresponding␈α⊂relative␈α∂minimal
␈↓ α∧␈↓entailment.␈α
 Thus␈α
we␈α
may␈α
care␈α
about␈α
minimality␈α∞and␈α
Occam's␈α
razor␈α
only␈α
over␈α
a␈α
certain␈α∞part␈α
of
␈↓ α∧␈↓our knowledge.

␈↓ α∧␈↓␈↓ αTNote␈α⊂that␈α⊂we␈α⊂may␈α⊂discover␈α⊂a␈α⊂set␈α⊂of␈α⊂facts␈α⊂one␈α⊂at␈α⊂a␈α⊂time␈α⊂so␈α⊂that␈α⊂we␈α⊂have␈α⊂an␈α⊂increasing
␈↓ α∧␈↓sequence␈α⊂␈↓↓A␈↓β1␈↓↓␈α⊂⊂␈α⊂A␈↓β2␈↓␈α⊂⊂␈α⊂...␈α⊂of␈α⊂sets␈α⊂of␈α⊂sentences.␈α⊂ A␈α⊂given␈α⊂sentence␈α⊂␈↓↓p␈↓␈α⊂may␈α⊂oscillate␈α⊂in␈α⊃its␈α⊂minimal
␈↓ α∧␈↓entailment␈α∂by␈α∞the␈α∂␈↓↓A␈↓βi␈↓,␈α∞e.g.␈α∂we␈α∞may␈α∂have␈α∂␈↓↓A␈↓β1␈↓π q␈↓βm␈↓↓ p␈↓,␈α∞␈↓↓A␈↓β2␈↓π q␈↓βm␈↓↓ ¬p␈↓,␈α∂neither␈α∞may␈α∂be␈α∞entailed␈α∂by␈α∂␈↓↓A␈↓β3␈↓,␈α∞etc.
␈↓ α∧␈↓The␈α
common␈α∞sense␈α
Occam's␈α∞razor␈α
conclusion␈α
about␈α∞a␈α
sentence␈α∞␈↓↓p␈↓␈α
often␈α
behaves␈α∞this␈α
way␈α∞as␈α
our
␈↓ α∧␈↓knowledge increases.

␈↓ α∧␈↓␈↓ αTReasons␈α
can␈α
be␈α
used␈α
to␈αreduce␈α
propositional␈α
circumscription␈α
to␈α
domain␈αcircumscription.␈α
 We
␈↓ α∧␈↓introduce␈αfor␈αeach␈α
propositional␈αletter␈α␈↓↓p␈↓βi␈↓␈αto␈α
be␈αminimized␈αa␈α
corresponding␈αpredicate␈α␈↓↓pr␈↓βi␈↓↓(r)␈↓␈αand␈α
the
␈↓ α∧␈↓axiom

␈↓ α∧␈↓1)␈↓ αt ␈↓↓p␈↓βi␈↓↓ ≡ ∃r.pr␈↓βi␈↓↓(r)␈↓,

␈↓ α∧␈↓which asserts that ␈↓↓p␈↓βi␈↓ is true only if there is a reason why.  We also need axioms
␈↓ α∧␈↓␈↓ u6


␈↓ α∧␈↓2)␈↓ αt ␈↓↓∀r.¬(pr␈↓βi␈↓↓(r) ∧ pr␈↓βj␈↓↓(r))␈↓

␈↓ α∧␈↓for␈α
each␈α␈↓↓i␈↓␈α
and␈α
␈↓↓j␈↓␈αand␈α
axioms␈α
asserting␈αthat␈α
reasons␈α
␈↓↓r␈↓␈αare␈α
distinct␈α
from␈αany␈α
other␈α
individuals.␈α A
␈↓ α∧␈↓minimal␈αmodel␈αwill␈αthen␈αhave␈αas␈αfew␈αreasons␈αas␈αpossible␈αand␈αhence␈αwill␈αminimize␈αthe␈αset␈αof␈αtrue
␈↓ α∧␈↓␈↓↓p␈↓βi␈↓s.
␈↓ α∧␈↓␈↓ u7


␈↓ α∧␈↓αCircumscription in the Blocks World

␈↓ α∧␈↓␈↓ αTHere␈α
is␈αa␈α
formalization␈αof␈α
the␈αblocks␈α
world␈αin␈α
which␈αcircumscription␈α
is␈αused␈α
to␈α
keep␈αopen
␈↓ α∧␈↓the␈α
set␈α
of␈α
possible␈α
circumstances␈α
that␈α
may␈α
prevent␈α
a␈α
block␈α
␈↓↓x␈↓␈α
from␈α
being␈α
moved␈α
onto␈α
a␈α∞block␈α
␈↓↓y.␈↓
␈↓ α∧␈↓We use the situation calculus of (McCarthy and Hayes 1969).

␈↓ α∧␈↓␈↓ αTA␈α
situation␈α
␈↓↓s␈↓␈α
is␈α
a␈α
snapshot␈α
of␈α
the␈α
world␈α
at␈α
an␈α
instant␈α
of␈α
time.␈α
 We␈α
write␈α
␈↓↓on(x,y,s)␈↓␈α
to␈αsay
␈↓ α∧␈↓that␈αblock␈α␈↓↓x␈↓␈αis␈αon␈α
block␈α␈↓↓y␈↓␈αin␈αsituation␈α␈↓↓s.␈↓␈α␈↓↓s' = move(x,y,s)␈↓␈α
is␈αthe␈αnew␈αsituation␈α␈↓↓s'␈↓␈αthat␈α
results␈αthe
␈↓ α∧␈↓action␈α∞of␈α∞moving␈α∞block␈α∞␈↓↓x␈↓␈α∞onto␈α∞block␈α∞␈↓↓y␈↓␈α
in␈α∞situation␈α∞␈↓↓s␈↓␈α∞is␈α∞attempted.␈α∞ If␈α∞the␈α∞preconditions␈α∞for␈α
the
␈↓ α∧␈↓action to be successful are satisfied, we will have ␈↓↓on(x,y,s')␈↓.

␈↓ α∧␈↓␈↓ αTWe␈α
begin␈α
with␈α
a␈α
static␈α
world,␈α
in␈α
which␈α
we␈α
want␈α
to␈α
use␈α
circumscription␈α
to␈α
avoid␈αstating␈α
more
␈↓ α∧␈↓on-ness relations than necessary.  Specifically, we would like circumscription to give us

␈↓ α∧␈↓␈↓ αT1. A block is clear unless contrary evidence exists.

␈↓ α∧␈↓␈↓ αT2. A block is on the table unless contrary evidence exists.

␈↓ α∧␈↓␈↓ αT3. Only those blocks exist for which there is evidence.

␈↓ α∧␈↓␈↓ αTSuppose␈α∞we␈α
have␈α∞sentences␈α
␈↓↓on(A,B),␈↓␈α∞␈↓↓on(B,C)␈↓␈α
and␈α∞␈↓↓on(D,E),␈↓␈α
where␈α∞␈↓↓A,␈↓␈α
...␈α∞,␈α
␈↓↓E␈↓␈α∞are␈α
specific
␈↓ α∧␈↓blocks.  We have the axiom

␈↓ α∧␈↓␈↓ αT␈↓↓∀x.(x ≠ Table ⊃ ∃y.on(x,y))␈↓

␈↓ α∧␈↓asserting that every block except the table is supported.  The axiom schema

␈↓ α∧␈↓␈↓ αT␈↓↓␈↓	F␈↓↓(A,B) ∧ ␈↓	F␈↓↓(B,C) ∧ ␈↓	F␈↓↓(D,E) ⊃ ∀x y.(on(x,y) ∧ y ≠ Table ⊃ ␈↓	F␈↓↓(x,y))␈↓

␈↓ α∧␈↓insures␈α∪that␈α∪the␈α∪only␈α∪␈↓↓on(x,y)␈↓␈α∪relations␈α∪are␈α∪those␈α∪explicitly␈α∪stated␈α∪except␈α∪that␈α∪all␈α∪blocks␈α∩not
␈↓ α∧␈↓mentioned as on something else are on the table.

␈↓ α∧␈↓␈↓ αTThe effect of motion is given by

␈↓ α∧␈↓␈↓ αT␈↓↓∀x y s.(movable(x,y,s) ⊃ on(x,y,move(x,y,s))␈↓.

␈↓ α∧␈↓There are various known causes of immovability.  Thus we may have

␈↓ α∧␈↓␈↓ αT␈↓↓∀x y z s.(on(z,x,s) ⊃ ¬movable(x,y,s))␈↓,

␈↓ α∧␈↓␈↓ αT␈↓↓∀x y z s.(on(z,y,s) ⊃ ¬movable(x,y,s))␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓∀x y s.(tooheavy x ⊃ ¬movable(x,y,s))␈↓.

␈↓ α∧␈↓If␈αthese␈αare␈αall␈αthe␈αcauses␈αof␈αimmovability␈αthat␈αwe␈αwish␈αto␈αtake␈αinto␈αaccount,␈αwe␈αmay␈αcombine␈αthe
␈↓ α∧␈↓above into a single sentence

␈↓ α∧␈↓3)␈↓ αt ␈↓↓∀s x y z.(on(z,x,s) ∨ on(z,y,s) ∨ tooheavy x ⊃ ¬movable(x,y,s))␈↓.
␈↓ α∧␈↓␈↓ u8


␈↓ α∧␈↓The converse of (3) may be written as a circumscription in the form

␈↓ α∧␈↓␈↓ αT␈↓↓∀s.[∀x␈α∂y␈α∂z.[on(z,x,s)␈α∂∨␈α∂on(z,y,s)␈α∂∨␈α∂tooheavy␈α∂x␈α∂⊃␈α∂␈↓	F␈↓↓(x,y,s)]␈α∂⊃␈α∂⊃␈α∂∀x␈α∂y.[¬movable(x,y,s)␈α∂⊃
␈↓ α∧␈↓↓␈↓	F␈↓↓(x,y,s)]]␈↓.

␈↓ α∧␈↓Of course, the converse can be written directly as

␈↓ α∧␈↓4)␈↓ αt ␈↓↓∀s x y z.(¬movable(x,y,s) ⊃ on(z,x,s) ∨ on(z,y,s) ∨ tooheavy x)␈↓.

␈↓ α∧␈↓Thus␈αcircumscription␈αis␈αa␈αkind␈αof␈αconverse␈αand␈αrequires␈αa␈αschema␈αto␈αexpress␈αit␈αonly␈αwhen␈αthe␈αset
␈↓ α∧␈↓of objects to be circumscribed is inductively defined.


␈↓ α∧␈↓αComparison with other formalisms

␈↓ α∧␈↓␈↓ αT1. Default cases.  Many programs provide default cases.

␈↓ α∧␈↓1.␈α∞Maybe␈α∂we␈α∞can␈α∞consider␈α∂propositional␈α∞and␈α∂domain␈α∞circumscription␈α∞as␈α∂instances␈α∞of␈α∂a␈α∞common
␈↓ α∧␈↓concept␈α⊃if␈α⊃we␈α⊂allow␈α⊃ourselves␈α⊃to␈α⊂introduce␈α⊃an␈α⊃arbitrary␈α⊂partial␈α⊃ordering␈α⊃of␈α⊂models␈α⊃of␈α⊃sets␈α⊂of
␈↓ α∧␈↓sentences␈α
and␈α
consider␈α
minimal␈α
models␈α
with␈αrespect␈α
to␈α
this␈α
ordering.␈α
 We␈α
probably␈α
want␈αto␈α
restrict
␈↓ α∧␈↓the␈α⊃ordering␈α⊃so␈α⊃that␈α⊃there␈α⊃will␈α⊃be␈α⊃some␈α⊃syntactic␈α⊃counterpart␈α⊃of␈α⊃minimal␈α⊃inference.␈α⊃ Actually
␈↓ α∧␈↓propositional␈αcircumscription␈α
doesn't␈αmeet␈α
this␈αrequirement␈αwithout␈α
modification,␈αbut␈α
anyway␈αit's
␈↓ α∧␈↓desirable.

␈↓ α∧␈↓2.␈α
Perhaps␈αthe␈α
right␈α
way␈αto␈α
reduce␈αpropositional␈α
circumscription␈α
to␈αdomain␈α
circumscription␈α
is␈αto
␈↓ α∧␈↓replace␈α∞each␈α
propositional␈α∞variable␈α∞␈↓↓p␈↓βi␈↓␈α
by␈α∞the␈α∞wff␈α
␈↓↓∃x.(index␈α∞x␈α
=␈α∞i)␈↓.␈α∞ In␈α
that␈α∞way␈α∞minimizing␈α
the
␈↓ α∧␈↓truth␈αof␈α
the␈αproposition␈αis␈α
accomplished␈αby␈αminimizing␈α
the␈αexistence␈αof␈α
the␈α␈↓↓x␈↓'s.␈α The␈α
purpose␈αof
␈↓ α∧␈↓␈↓↓index␈αx␈α=␈αi␈↓␈αis␈αto␈αmake␈αsure␈αthat␈αthe␈αexistence␈αof␈αthe␈α␈↓↓x␈↓'s␈αcan␈αbe␈αminimized␈αseparately.␈α We␈αneed␈αto
␈↓ α∧␈↓be␈αsure␈αthat␈αno␈αother␈αobject␈αhas␈αan␈αinteger␈αindex,␈αbut␈αwe␈αcan␈αintroduce␈αaxioms␈αthat␈αrequire␈α
them
␈↓ α∧␈↓all to have the non-integer JUNK as index.

␈↓ α∧␈↓This␈α⊃raises␈α⊃the␈α⊂problem␈α⊃of␈α⊃whether␈α⊃there␈α⊂is␈α⊃an␈α⊃analogous␈α⊂way␈α⊃of␈α⊃treating␈α⊃predicates␈α⊂␈↓↓p(u,v)␈↓.
␈↓ α∧␈↓Maybe␈αwe␈αwant␈αto␈αreplace␈αit␈αby␈α␈↓↓∃x.(p'(u,v,x) ∧ index x = i)␈↓␈αor␈αperhaps␈αistead␈αof␈α␈↓↓ = i␈↓,␈αwe␈αshould
␈↓ α∧␈↓have ␈↓↓ = <u,v,i>␈↓.

␈↓ α∧␈↓3. CIRCUM[1,CLT] is the following example:

␈↓ α∧␈↓Consider the following problem (told to CLT by DrewMcD, ascribed to Bmoore):

␈↓ α∧␈↓You␈α∞are␈α∞told␈α∞that␈α∞the␈α∞only␈α∞things␈α∞on␈α∞the␈α∞table␈α∞are␈α∞things␈α∞that␈α∞you␈α∞can␈α∞prove␈α∞are␈α∞on␈α∞the␈α
table.
␈↓ α∧␈↓Further␈αyou␈αare␈αtold␈αthat␈αA␈αis␈αon␈αthe␈αtable␈αand␈αB␈αis␈αon␈αthe␈αtable␈αand␈αthat␈αthere␈αis␈αsomething␈αred
␈↓ α∧␈↓on the table.  You would like to be able to conclude that either A is red or B is red.

␈↓ α∧␈↓Circumscription␈α
can␈α
be␈α
applied␈α
to␈α
solve␈α
this␈αproblem.␈α
 We␈α
formalize␈α
the␈α
problem␈α
in␈α
a␈αlanguage
␈↓ α∧␈↓L=<<Ontable,Red>,<>,<A,B>> where Ontable and Red are unary.  The theory is:

␈↓ α∧␈↓␈↓ αT(1) Ontable(A)

␈↓ α∧␈↓␈↓ αT(2) Ontable(B)
␈↓ α∧␈↓␈↓ u9


␈↓ α∧␈↓␈↓ αT(3) ∃x.(Ontable(x)∧Red(x))

␈↓ α∧␈↓␈↓ αTCircumscribing with respect to (1) and (2) we obtain the schema:

␈↓ α∧␈↓␈↓ αT(4) ␈↓	F␈↓(A)∧␈↓	F␈↓(B) ⊃ ∀x.␈↓	F␈↓(x)

␈↓ α∧␈↓␈↓ αTand it is easy to jump to the conclusion that

␈↓ α∧␈↓␈↓ αT(5) ∀x.(x=A∨x=B)

␈↓ α∧␈↓␈↓ αTand thus to conclude that Red(A)∨Red(B).

␈↓ α∧␈↓␈↓ αTNotice␈α⊃that␈α∩if␈α⊃the␈α∩circumscription␈α⊃is␈α∩done␈α⊃with␈α∩respect␈α⊃to␈α∩all␈α⊃three␈α∩facts␈α⊃then␈α∩we␈α⊃lose.
␈↓ α∧␈↓Namely we get the schema

␈↓ α∧␈↓␈↓ αT(6) ␈↓	F␈↓(A)∧␈↓	F␈↓(B)∧∃x.(␈↓	F␈↓(x)∧Ontable(x)∧Red(x)) ⊃ ∀x.␈↓	F␈↓(x)

␈↓ α∧␈↓␈↓ αTthen we only conclude

␈↓ α∧␈↓␈↓ αT(7) ∀x.(x=A∨x=B∨Red(x))

␈↓ α∧␈↓␈↓ αTwhich does not allow us to show that either A or B is red.

␈↓ α∧␈↓␈↓ αT4.␈α⊃The␈α∩essence␈α⊃of␈α∩the␈α⊃Moore-McDermott␈α⊃example␈α∩is␈α⊃included␈α∩in␈α⊃the␈α∩following␈α⊃simpler
␈↓ α∧␈↓example.

␈↓ α∧␈↓␈↓ αTThere␈αis␈αone␈αconstant␈αA␈αand␈αone␈αsentence␈α∃x.Red(x).␈α Circumscribing␈αon␈αthe␈α
constant␈αonly
␈↓ α∧␈↓gives␈α␈↓	F␈↓(A)␈α⊃␈α∀x.␈↓	F␈↓(x)␈αand␈αspecializing␈α␈↓	F␈↓␈αby␈α
∀x.(␈↓	F␈↓(x)␈α≡␈αx␈α=␈αA)␈αestablishes␈α∀x.(x␈α=␈αA)␈α
from␈αwhich
␈↓ α∧␈↓Red(A) follows.  Circumscribing on both A and ∃x.Red(x) gives

␈↓ α∧␈↓␈↓ αT␈↓	F␈↓(A) ∧ ∃x.(␈↓	F␈↓(x) ∧ Red(x)) ⊃ ∀x.␈↓	F␈↓(x)

␈↓ α∧␈↓␈↓ αTfrom which it doesn't look like we can infer Red(A).

␈↓ α∧␈↓␈↓ αTIt␈α∂looks␈α∂like␈α∞circumscription␈α∂doesn't␈α∂give␈α∞us␈α∂what␈α∂is␈α∞true␈α∂in␈α∂all␈α∞minimal␈α∂models␈α∂but␈α∞only
␈↓ α∧␈↓what␈αis␈αtrue␈αin␈αall␈αminimal␈αmodels␈αcontained␈αin␈αarbitrary␈αmodels,␈αi.e.␈αa␈αsentence␈αp␈αis␈αprovable␈αby
␈↓ α∧␈↓circumscribing␈αa␈αset␈αof␈αsentences␈αA␈αiff␈αevery␈αmodel␈αM␈αof␈αA␈αis␈αsuch␈αthat␈αevery␈αminimal␈αmodel␈αM'
␈↓ α∧␈↓of␈αA␈αcontained␈αin␈αM␈αsatisfies␈αp.␈α THE␈αABOVE␈αWAS␈αA␈αMISTAKE.␈α At␈αleast␈αin␈αthe␈αabove␈αcase
␈↓ α∧␈↓the model with two objects - A and a red one - is indeed minimal w/r {A , ∃x.Red(x)}.

␈↓ α∧␈↓␈↓ αT5.␈αImitation␈αsemantics.␈α Suppose␈αwe␈αreplace␈αsome␈αof␈αthe␈αpredicate␈αsymbols␈αof␈αa␈αtheory␈αby␈αa
␈↓ α∧␈↓new␈αsymbols␈αwith␈αone␈αmore␈αargument␈α-␈αa␈αworld.␈α Thus␈αRed(x)␈αis␈αreplaced␈αby␈αRed(x,w).␈α Some␈αof
␈↓ α∧␈↓the␈α∞properties␈α∞of␈α
model␈α∞theory␈α∞can␈α∞now␈α
be␈α∞axiomatized␈α∞within␈α∞the␈α
theory.␈α∞ The␈α∞process␈α∞can␈α
be
␈↓ α∧␈↓repeated␈α⊂by␈α⊃adding␈α⊂another␈α⊂"outer"␈α⊃world␈α⊂parameter,␈α⊂but␈α⊃we␈α⊂shall␈α⊂discuss␈α⊃only␈α⊂a␈α⊃single␈α⊂such
␈↓ α∧␈↓"semanticization" to begin with.

␈↓ α∧␈↓␈↓ αTEvery␈αterm␈αand␈α
wff␈αnow␈αdepends␈αon␈α
w␈α-␈αassuming,␈α
as␈αwe␈αshall␈αfor␈α
now,␈αthat␈αwe␈αapply␈α
each
␈↓ α∧␈↓predicate␈α⊂to␈α∂the␈α⊂same␈α∂variable␈α⊂w␈α∂as␈α⊂we␈α∂build␈α⊂up␈α∂the␈α⊂wffs.␈α∂ We␈α⊂can␈α∂quantify␈α⊂over␈α∂w,␈α⊂so␈α∂that
␈↓ α∧␈↓∀w.<wff>␈α⊃will␈α∩enjoy␈α⊃some␈α⊃of␈α∩the␈α⊃properties␈α⊃of␈α∩validity␈α⊃and␈α⊃∃w.<wff>␈α∩will␈α⊃have␈α⊃some␈α∩of␈α⊃the
␈↓ α∧␈↓properties of satisfiability.
␈↓ α∧␈↓␈↓ f10


␈↓ α∧␈↓␈↓ αTHow␈α⊃to␈α∩axiomatize␈α⊃w␈α∩is␈α⊃not␈α∩immediately␈α⊃obvious.␈α⊃ One␈α∩idea␈α⊃is␈α∩to␈α⊃imagine␈α∩a␈α⊃common
␈↓ α∧␈↓domain␈α∞of␈α∞non-w␈α
s␈α∞and␈α∞introduce␈α∞a␈α
predicate␈α∞exists(x,w).␈α∞ (I␈α∞confess␈α
a␈α∞weakness␈α∞for␈α∞theories␈α
in
␈↓ α∧␈↓which something like existence is a predicate).  This allows a definition of ordering

␈↓ α∧␈↓␈↓ αT␈↓↓w1 < w2 ≡ ∀x.(exists(x,w1) ⊃ exists(x,w2))
␈↓ α∧␈↓␈↓ αT∧ ∀xy.(exists(x,w1) ∧ exists(y,w1) ⊃ (P(x,y,w1) ≡ P(x,y,w2))
␈↓ α∧␈↓␈↓ αT∧ ...


␈↓ α∧␈↓␈↓ αTwhere␈α...␈αindicates␈α
that␈αthere␈αis␈αa␈α
wff␈αsimilar␈αto␈α
that␈αon␈αthe␈αsecond␈α
line␈αfor␈αeach␈αpredicate␈α
in
␈↓ α∧␈↓the language.  This will permit us to define minimal worlds.

␈↓ α∧␈↓␈↓ αTOur␈αability␈αto␈αimitate␈αreal␈αmodel␈αtheory␈αwill␈αdepend␈αon␈αour␈αtools␈αfor␈αasserting␈αthe␈αexistence
␈↓ α∧␈↓of␈α∞enough␈α∞worlds.␈α∞ If␈α
the␈α∞domain␈α∞is␈α∞infinite␈α
and␈α∞there␈α∞is␈α∞even␈α
one␈α∞unary␈α∞predicate␈α∞symbol,␈α
the
␈↓ α∧␈↓number␈α∪of␈α∪interpretations␈α∩is␈α∪already␈α∪non-denumerable,␈α∩and␈α∪the␈α∪Lowenheim-Skolem␈α∩theorem
␈↓ α∧␈↓already tells us that no axiomatization can insure that.

␈↓ α∧␈↓␈↓ αTA␈α
certain␈α
amount␈α
can␈α
be␈α
done␈α
by␈α
postulating␈α
that␈α
for␈α
every␈α
world␈α
w␈α
there␈α
is␈α
a␈α
world␈α
w'␈α
that
␈↓ α∧␈↓gives␈α
the␈α
same␈α
value␈α
to␈α
all␈α
predicates␈α
except␈α
that␈α
a␈α
single␈α
predicate␈α
has␈α
a␈α
single␈α
value␈αchanged.
␈↓ α∧␈↓We␈α
can␈α
also␈α
imagine␈α
other␈α
changes␈α
whose␈α∞possibility␈α
can␈α
be␈α
stated.␈α
 The␈α
main␈α
purpose␈α∞of␈α
such
␈↓ α∧␈↓axiomatizations␈α↔will␈α⊗be␈α↔to␈α⊗insure␈α↔that␈α⊗certain␈α↔formulas␈α⊗or␈α↔at␈α⊗least␈α↔enough␈α↔formulas␈α⊗are
␈↓ α∧␈↓"satisfiable".

␈↓ α∧␈↓␈↓ αT"Completeness" can also be defined as asserting that all "valid" formulas are provable.

␈↓ α∧␈↓␈↓ αTI think all this is related to circumscription, but I can't now make the connection.

␈↓ α∧␈↓␈↓ αT6. Propositional circumscription can be done by introducing worlds as follows:

␈↓ α∧␈↓␈↓ αTEach propositional variable ␈↓↓p␈↓βi␈↓ is replaced by a function ␈↓↓p␈↓βi␈↓↓(w)␈↓.

␈↓ α∧␈↓␈↓ αTWe write

␈↓ α∧␈↓␈↓ αT␈↓↓w1 ≤ w2 ≡ ∀i.[p␈↓βi␈↓↓(w1) ⊃ p␈↓βi␈↓↓(w2)]␈↓

␈↓ α∧␈↓␈↓ αTwhere␈αwe␈αmay␈αsuppose␈αthat␈αthe␈αquantification␈αover␈α␈↓↓i␈↓␈αactually␈αdesignates␈αa␈αconjunction␈αover
␈↓ α∧␈↓the set of propositional variables to be circumscribed.

␈↓ α∧␈↓␈↓ αTMinimality is defined by

␈↓ α∧␈↓␈↓ αT␈↓↓minimal w ≡ ∀w1.(w1 ≤ w ⊃ w1 = w)␈↓.

␈↓ α∧␈↓␈↓ αTA wff in the original formulation becomes a ␈↓↓wff(w)␈↓ in the new.  We write ␈↓↓wff1 ␈↓πq␈↓↓ wff2␈↓ if

␈↓ α∧␈↓␈↓ αT␈↓↓∀w.(wff1(w) ∧ minimal w ⊃ wff2(w))␈↓.

␈↓ α∧␈↓␈↓ αT5. Further note on propsitional circumscription

␈↓ α∧␈↓␈↓ αTPerhaps␈α∞the␈α∂right␈α∞analog␈α∂of␈α∞the␈α∂␈↓	F␈↓␈α∞of␈α∂domain␈α∞circumscription␈α∂is␈α∞to␈α∂replace␈α∞a␈α∂formula␈α∞by
␈↓ α∧␈↓␈↓ f11


␈↓ α∧␈↓another␈α∀that␈α∃contains␈α∀a␈α∃free␈α∀propositional␈α∃parameter␈α∀-␈α∃call␈α∀it␈α∃π.␈α∀ Circumscribing␈α∃sets␈α∀this
␈↓ α∧␈↓parameter to whatever value is convenient.  Thus suppose we have

␈↓ α∧␈↓␈↓ αT␈↓↓leakyboat ⊃ cantgo␈↓,

␈↓ α∧␈↓␈↓ αTand␈α⊃we␈α⊃either␈α⊃do␈α⊃or␈α⊃don't␈α⊃have␈α⊃the␈α⊃additional␈α⊃formula␈α⊃␈↓↓leakyboat␈↓.␈α⊃ The␈α⊂circumscription
␈↓ α∧␈↓formula should then be either

␈↓ α∧␈↓␈↓ αT␈↓↓leaky ∧ (leaky ⊃ π) ⊃ (π ⊃ cantgo)␈↓

␈↓ α∧␈↓␈↓ αTor just

␈↓ α∧␈↓␈↓ αT5)␈↓ αt ␈↓↓(leaky ⊃ π) ⊃ (π ⊃ cantgo)␈↓.

␈↓ α∧␈↓␈↓ αTIn␈αthe␈αformer␈αcase,␈αtaking␈απ␈αto␈αbe␈αfalse␈αleads␈αto␈αa␈αtautology,␈αsince␈αthe␈αleft␈αside␈αof␈α
the␈αmain
␈↓ α∧␈↓implication is false.  In the second case it leads to the converse

␈↓ α∧␈↓␈↓ αT␈↓↓¬leakyboat ⊃ ¬cantgo␈↓

␈↓ α∧␈↓␈↓ αTwhich is a step in the right direction anyway.  Where (5) is to come from is still not clear.

␈↓ α∧␈↓This version of MINIMA.NEW[S79,JMC] PUBbed at 18:37 on July 7, 1979.